A, B:Type. (A r B)  (x, y:A. (x = y  B)  (x = y))  EqDecider(B)  EqDecider(A) 

latex

Definitions	x:A. B(x), P  Q, S  T, EqDecider(T), P  Q, t  T, , P & Q, P  Q, suptype(S; T)
Lemmas	bool wf, iff wf, assert wf, rev implies wf